$\forall$$A$:Type, $F$:($t$:$\mathbb{N}\rightarrow$($\mathbb{N}$$_{\mbox{\scriptsize $<$$t$}}$$\rightarrow$$A$)$\rightarrow$$A$). CV($F$) $\in$ $\mathbb{N}\rightarrow$$A$